\chapter{Introduction}
As computer systems are entrusted with more and more sensitive and personal
information, the need to effectively control access to the data becomes
increasingly important. Recent revelations about very sophisticated and
targeted attacks as well as broad, nation-wide surveillance programs seriously
call the effectiveness of currently deployed security systems in question.

A common defense strategy is to compartmentalize information and its processing.
An example would be the usage of a dedicated computer for Internet banking that
is only connected to the Internet when needed. However, this approach does not
scale well, since this would necessitate having a separate device for each task
that should be performed in some form of isolation.

A separation kernel (SK)\index{SK}\index{separation kernel} is a specialized
microkernel\index{microkernel} which provides an execution environment for
components that can only communicate according to a given policy and are
otherwise isolated from each other. This isolation also includes the limitation
of potential side- and covert channels. A SK can serve as a basis for the
implementation of a component-based system.

Related problems can arise in cloud services, where multiple unaffiliated parties
share the same physical machine but are to be separated from each other so as to
not (involuntarily) share any data. Recent attacks
\cite{Wu:2012:WHH:2362793.2362802} have demonstrated that current solutions do
not provide the necessary degree of isolation. Since the adoption of
virtualization\index{virtualization}, especially in the field of cloud
computing, has rapidly increased in the past years, chip manufacturers such as
Intel are extending their processors with advanced hardware virtualization
features.

Another issue is the complexity associated with developing security systems
that must exhibit very strong robustness and provide high
assurance\index{assurance}. Tools and methods such as formal
verification\index{formal verification} exist, but are generally disregarded. A
small code base results in better verifiability since the complexity of the
software should be manageable and the effort needed for review is greatly
reduced.

The SPARK\index{SPARK} programming language is used for the development of
industrial high integrity projects. It provides the means to prove certain
properties of the code and its track record
\cite{Chapman:2000:IES:369264.369270} shows that it can be used to effectively
implement real-world systems.

All these recent developments provide a good setting for the design and
implementation of an open-source separation kernel. Using hardware
virtualization features for component separation and leveraging Intel's latest
processor features should allow to implement a small kernel suitable for formal
verification. Using SPARK as the programming language greatly increases the
confidence in the implementation since it eliminates complete categories of
common programming errors, e.g. buffer overflows. Making the source code and
technical documentation publicly available enables third-party review.

This document presents the design and implementation of the Muen separation
kernel, which was developed during the course of our master thesis.

\section{Notation}
This section presents the notational conventions used throughout this document.

\paragraph{Keywords}
Important terms and concepts that are introduced for the first time are
presented in \emph{italic style}. Subsequent occurrences of the same term have
no special formatting. The same style is also used to \emph{emphasize} words in
the text.

\paragraph{Numbers}
Regular numbers that have no leading special character are expressed as decimal
values. Hexadecimal numbers such as memory addresses are explicitly preceded by
\texttt{0x}.

\paragraph{Units}
Storage units such as kilo-, mega- and gigabyte are designated by
the common abbreviations KB, MB and GB.

\paragraph{Tools and Procedures}
References to subroutines and keywords of a programming language, as well as
command line tools are formatted in \texttt{typewriter} style.

\section{Related Literature}
Since the target hardware platform of the separation kernel is the Intel x86
architecture, its specification called "Intel\textsuperscript{\textregistered}
64 and IA-32 Architectures Software Developer's Manual"
\cite{IntelSDM}\index{Intel SDM} is the main source of technical information
concerning the hardware platform. The documents are commonly referred to by
their short name \emph{Intel SDM}.

The books are available online and updated by Intel on a regular basis. This
can lead to changes in the document structure. The chapter and section
citations given in this report refer to the Intel SDM revision 44, released in
August 2012.

\section{Provenance of Name}
\emph{Muen}\index{Muen} is Japanese and translates to "unrelated/without
relation". It was chosen since it is a fitting allegory of the components
isolated by the separation kernel. Figure \ref{fig:muen} depicts the word in
Japanese kanji characters\footnote{The Unicode code points of the two characters
are U+28961 U+32257.}.

\begin{figure}[h]
	\centering
	\includegraphics[scale=0.4]{images/muen.pdf}
	\caption{Muen in kanji}
	\label{fig:muen}
\end{figure}

The root of the word Muen is "Mu" which denotes a negative: the absence of
everything. It is a keyword in Chan and Zen Buddhism and also mentioned in the
Jargon File \cite{jargonfile}.
